A:Type, I:MaInterface(A), i:Id.
(i  ma-interface-locs(I))
 (ma-interface-conds(I;i)  k:Knd fp V:Type  (State(ma-interface-ds(I;i))V(A + Top))) 

latex

Definitions	False, {x:A| B(x)} , left + right, P  Q, Dec(P), x:A. B(x), Knd, P  Q, (x  l), ma-interface-ds(I;i), t  T, State(ds), x:AB(x), Type, Top, x:A  B(x), type List, b, S  T, ma-interface-dom(I;i), ma-interface-code(I;i;k), ma-interface-valtype(I;i;k), <a, b>, x.A(x), ma-interface-conds(I;i), a:A fp B(a), Id, MaInterface(T)
Lemmas	ma-interface-valtype wf, ma-interface-code wf, l member wf, ma-interface-dom wf, decl-state wf, ma-interface-ds wf, decidable l member, decidable equal Kind